es:ES, A:Type, ds:x:Id fp Type, conds1, conds2:k:Knd fp V:Type  (State(ds)V(A + Top)), i:Id.
es-triggers-params-consistent(es;A;i;ds;conds1)
 es-triggers-params-consistent(es;A;i;ds;conds2)
 conds1 || conds2
 ([es-triggers(es;i;ds;conds1)?es-triggers(es;i;ds;conds2)]
 (=
 (es-triggers(es;i;ds;conds1  conds2)
 ( AbsInterface(A)) 

latex

Definitions

x. t(x), x:A. B(x), P  Q, P  Q, P  Q, P & Q, P  Q, , t  T, Top, ff, tt, if b then t else f fi , True, T, state@i, State(ds), x(s), x:A. B(x), Knd, {T}, SQType(T), do-apply(f;x), can-apply(f;x), X(e), e  X, es-triggers(es;i;ds;conds), p  q, isl(x), b, False, Unit, , A, f || g, es-triggers-params-consistent(es;A;i;ds;conds), A c B, , fpf-domain(f)

Lemmas

es-interface-conditional-domain-iff, iff functionality wrt iff, all functionality wrt iff, es-is-interface wf, assert wf, iff wf, es-is-interface-triggers2, fpf-domain wf, l member wf, es-kind wf, fpf-trivial-subtype-top, fpf-domain-join, fpf-join-ap-sq, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, bool wf, fpf-dom wf, member-fpf-domain, not functionality wrt iff, top wf, isl wf, true wf, squash wf, subtype rel self, es-vartype wf, subtype rel dep function, es-state-when wf, pi2 wf, decl-state wf, and functionality wrt iff, Id sq, exists functionality wrt iff, IdLnk wf, es-state-subtype-iff, Kind-deq wf, member-fpf-dom, es-val wf, bool sq, bool cases, assert-eq-id, es-loc wf, eq id wf, fpf-join wf, fpf-ap wf, outl wf, fpf-join-dom, false wf, fpf-join-dom2